i:Id. onceR{a:ut2, done:ut2}(i)  es_realizer{i:l} 

latex

Definitions	decl-type{i:l}(ds; x), if b then t else f fi , top, x. t(x), tt, es-state-ap(s; x), onceR{$a:ut2, $done:ut2}(i), t  T, x:A. B(x), x(s), decl-state(ds)
Lemmas	Rframe wf, decl-type wf, fpf-cap-single1, btrue wf, locl wf, Reffect wf, Rinit wf, bool wf, subtype rel self, eqof eq btrue, id-deq wf, fpf-cap-single, bnot wf, Id wf, fpf-single wf, Rpre wf, Rlist wf